…linearity to side condition

The same-account variant of #transferFunds was

    rule <k> #transferFunds ACCT ACCT VALUE => .K ... </k>
         ...
      requires VALUE <=Int ORIGFROM

i.e. the linearity guard `ACCT ACCT` required the two account-id
arguments to be syntactically identical. Booster's matcher cannot
discharge that on distinct-named symbolic variables (e.g.
`#transferFunds ?CONTRACT_ID 1 0`), even when the path constraint
implies their distinctness — match returns Indeterminate, booster
aborts, and the proof yields to kore.

Reformulate as

    rule <k> #transferFunds ACCTFROM ACCTTO VALUE => .K ... </k>
         ...
      requires ACCTFROM ==K ACCTTO andBool VALUE <=Int ORIGFROM

The LHS now uses distinct variable names so the match is unconditional;
the original linearity moves into the side condition as `==K`, which
booster can discharge via the path constraint (or via its SMT path)
without an indeterminate-match abort. Semantically equivalent on
concrete inputs and strictly more permissive on symbolic inputs in a
sound direction (matches when args are semantically equal but not
syntactically).

Recover-mode sweep identified 12 kore-execute handoffs (all benchmarks
ecrecover variants) caused by this exact match-fail abort. Validated
locally on benchmarks/ecrecover00-siginvalid-spec.k together with the
#asAccount [total] fix in the preceding commit: the spec's recover-mode
kcfg went from 2 kore-handoffs to 0, proof still passes.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
(cherry picked from commit 1bff5e84ed608edeeb5e403e748b342e40f33f4b)